i, x:Id, k:Knd, T:Type.
@i: only members of [k] affect x :T  Dsys
& (D:Dsys.
& (@i: only members of [k] affect x :T  D
& ( D 
& ( realizes es.
& ( vartype(i;x)  T
& ( & e@i.
& ( & ((x after e) = (x when e)  T  kind(e) = k  Knd)
& ( & & (kind(e) = k  (x after e) = (x when e)  T)) 

latex

Definitions	False, t  T, left+right, P  Q, P  Q, A, Type, Prop, x:A. B(x), ES(the_w), kind(e), Knd, s = t, x:AB(x), Void, Dec(P), x when e, (x after e), <a,b>, vartype(i;x), A & B, P & Q, type List, nil, (x  l), P  Q, x:AB(x), P  Q, {T}, car.cdr, loc(e), Id, E, e@i. P(e), @i only events in L change   x : T, PossibleWorld(D;w), FairFifo, World, D1  D2, Dsys, D realizes es. P(es)
Lemmas	s-frame-rule, dsys wf, d-sub wf, world wf, fair-fifo wf, possible-world wf, es-E wf, Id wf, es-loc wf, es-vartype wf, cons member, implies functionality wrt iff, not functionality wrt iff, or functionality wrt iff, nil member, l member wf, es-after wf, es-when wf, not wf, decidable equal Kind, Knd wf, es-kind wf, w-es wf, false wf